\section{SAT-based CSTE Planning Framework}\label{sec:encoding}

%*************************************************************************
%************************** Algorithm SCP ********************************
%*************************************************************************
\begin{algorithm}[t]
\LinesNumbered
\caption{A SAT-based CSTE Planning
\label{overall}
Framework (SCP)}

\KwIn{A CSTE planning problem: $\Pi$}

\KwOut{A solution plan}

transform durative actions into simple ones\;

% set $\delta$ as the step size\;

$N\leftarrow 0$\;

%$Z \leftarrow $ maximum makespan\;

\Repeat{a solution is found or search timeout}{
    $N\leftarrow N + 1$\;
    encode the problem into a MinCost SAT instance with makespan $N$\; %with partial order goal variables between $N-\delta+1$ and $N$\;
    optimally solve the encoded MinCost SAT instance\;
}

\eIf{a solution is found}{
    decode the solution and return\;
}{
    return with no solution\;
}
\end{algorithm}
%*************   End of algorithm    **********************************

We now formulate CSTE planning as an optimization problem with SAT
constraints, which we known as MinCost SAT.
Our overall planning algorithm is referred to as a SAT-based CSTE Planning (SCP) framework, shown in Algorithm~\ref{overall}.
Our planning framework follows the bounded SAT solving strategy, originally proposed in
SATPlan~\cite{Kautz92,Kautz96}. We start from a lower bound of the makespan (N=1),
encode the CSTE problem as a MinCost SAT instance, either prove it unsatisfiable or solve it
optimally (with respect to the MinCost SAT objective) for each
makespan, until a solution is found or the search times out.
%meet a pre-determined upper bound or find a solution or .

%to-do; R. Huang
%Usually a SAT-based planner~\cite may use heuristics, such as
%relaxed planning graph, to estimate a starting point of $N$.
%We do not apply such one here because
%Although there exists earlier research
%in applying planning graph to temporal planning, all existing works
%that we are aware of either have limited
%expressiveness~\cite{Smith99} or are unable to optimize time
%span~\cite{Long2003}. These two shortcomings may lead to an
%overestimation on step size even for the first iteration of the
%planning.


\subsection{Extended SAT formulations}

\nop{ In addition, we define MinCost SAT~\cite{Li04} and weighted
partial Max-SAT~\cite{maxsat09}, two extended forms of SAT
problems.}

We first present the SAT formulations.
A SAT problem is defined as $\Phi=(V,C)$, where $V$ is a set
of Boolean variables and $C$ is a set of clauses. A variable
assignment $\psi$ assigns each variable $x$ in $V$ to true or
false. Given a variable assignment $\psi$ and a variable $x\in V$, we
let the function $v_{\psi}(x)$ to be 1 when variable $x$ is true in the
variable assignment, or 0 otherwise. Likewise, given a variable
assignment $\psi$ and clause $p\in C$, we let $v_{\psi}(p)$ to be 1 when $p$
is satisfied by the variable assignment, or 0 otherwise. Given a SAT
problem $\Phi=(V,C)$, a valid solution is a variable assignment $\psi$,
such that for each $p\in C$, $v_{\psi}(p)=1$.


We use the notation of assignment function $\psi:V\cup C \rightarrow
\{0,1\}$ in  the following definitions. First, we define MinCost SAT
problems~\cite{Li04}.

\begin{defn}\em (MinCost SAT Problem)~\label{def:mincost}
A MinCost SAT problem is a tuple $\Phi^c=(V,C,\mu)$, where $V$ is a
set of Boolean variables, $C$ is a set of clauses, and $\mu$ is a
function $\mu: V \rightarrow \mathbb{N}$. A solution to
$\Phi$ is a variable assignment $\psi$ that minimizes the objective
function:
$$ cost(\psi) = \sum_{x\in{V}}{\mu(x)v_{\psi}(x)},$$
\hspace{16mm}subject to: $v_{\psi}(p)=1,\forall p\in C.$
\end{defn}

\nop{
Another extended SAT problem that we consider is the weighted partial
Max-SAT Problem~\cite{maxsat09}.


\begin{defn}\em (Weighted partial Max-SAT problem)~\label{def:maxsat}
A weighted partial Max-SAT problem is a tuple
$\Phi^{a}=(V,C^h,C^s,w)$,  where $V$ is a set of variables, $C^h$
and $C^s$ are sets of hard and soft clauses, respectively, and $w$ is the weight function
of soft clauses defined by $w: C^s \rightarrow \mathbb{N}$.

A solution to $\Phi^{a}$ is a variable assignment $\psi$ that maximizes the function:
$$ weight(\psi) = \sum_{p \in {C^s}}{w(p)v_{\psi}(p)},$$
\hspace{16mm}subject to:
$$v_{\psi}(p)=1,\forall p\in C^h.$$
\end{defn}


A weighted partial Max-SAT problem $\Phi^a$ amounts to
finding a variable assignment, such that all hard
clauses are satisfied, and the total weight of satisfied soft
clauses is maximized.
}

\subsection{Transformation of actions}

In the first step of our SCP framework (Algorithm~\ref{overall}),
each cost-sensitive durative action $o$ is converted to two simple
actions and one propositional fact, written as $(o_{\vdash},o_{\dashv},f^o)$.
We use the symbol $a$ to denote the simple action which indicates the
starting ($a = o_{\vdash}$) or ending events ($a = o_{\dashv}$) of $o$. The fact $f^o$, when is true,
indicates that $o$ is being executed. We denote the set of all such
$f^o$ as $F^o=\{ f^o \mid o\in O\}$. We further denote $pre(a)$,
$add(a)$ and $del(a)$ as the set of preconditions, the set of
add-effects and the set of delete-effects of a simple action $a$,
respectively. Note this transformation would only take effects on those actions with $\rho>1$. Otherwise, the durative action is just a simple action thus a transformation is not needed.

We transform a CSTE planning problem $\Pi=(I,F,O,G)$ into a
simplified planning problem $\Pi^s=(I,F^s,O^s,G)$, where $F^s = F\cup
F^o$ and $O^s = \{o_{\vdash},o_{\dashv}\mid o \in O \} \cup
\{ \textrm{no-op}~action~for~f\mid  f\in F^s\}$. The use of no-op actions
is a standard technique for SAT-based planning to handle the frame problem.
A no-op action for $f$ has no delete-effect and uses $f$ as its precondition and add-effect.
The cost of each simple action is defined as,
\[ \mu(a) = \left  \{
\begin{array}{ll}
   \mu(o),    & \mbox{ if $a = o_{\vdash}$ } \\
    0,          & \mbox{otherwise}\\
\end{array} \right. \]


The idea of transforming durative actions to simple actions was first proposed in~\cite{Long03}.
An advantage of this scheme is that some techniques from classical planning can be applied to the
transformed problem, such as encoding classic planning as SAT.
%Note that the transformation that we use is
%sound and complete, because it results in a simplified planning problem, along with extra
%constraints enforcing the temporal information.

Given the above representation, it is necessary to encode action
mutual exclusion (mutex) constraints to ensure the correctness of
solutions. An algorithm that detects mutexes between durative
actions in temporal planning is proposed in~\cite{Smith99}. We use
this algorithm to compute mutexes for all transformed actions $a \in
O^s$, which are included in the encoding.


\subsection{MinCost SAT encoding}

%After the above transformation,
For a CSTE problem instance $\Pi=(I,F,O,G)$ and the corresponding transformation $\Pi^s=(I,F^s,O^s,G)$, given a makespan $N$, we define a MinCost SAT problem $\Phi$ with the following variable set $V$ and clause set $C$.
The variable set $V$ includes two types of variables:

\begin{enumerate}
\item action variables $x_{a,t}$,~$0\le t < N,~a\in O^s$.
\item fact variables $x_{f,t}$,~$0\le t \le N,~f\in F^s$.
%\item goal set variables $W_{t}$, $N-\delta+1 \le t \le N$.
\end{enumerate}
Each variable in $V$ represents the assignment of an action or a fact at time $t$.

The clause set $C$ has the following clauses:
\begin{enumerate}
\item Initial state (for all $f\in I$):~$x_{f,0}$. All initial states must be true at time $0$.

\item Goal state (for all $g\in G$):~$x_{g,N}$. All goal states must be true at time $N$.
%Qiang 3.15 why delete this?
%\item Partial order goal states (for all $t\in[N-\delta+1,N]$):\\
%$W_t \rightarrow \bigwedge_{\forall f\in G} x_{f,t}$

\item Preconditions of simple actions (for all $a\in O^s$,~$0\le t < N$):
$$x_{a,t}\to \bigwedge_{f\in pre(a)}x_{f,t}$$
%$\neg x_{a,t} \begvee x_{f,t}$.\\
If an action is true at time $t$, then its precondition facts must be true at time $t$ too.

\item Add effects of simple actions (for all $f\in F^s$,~$0 < t \le N$):
$$x_{f,t} \to \bigvee_{\{a \mid f\in add(a)\}} x_{a,t-1}$$
%$\neg x_{f,t} \bigvee_{\forall a, f\in add(a)} x_{a,t-1}$
If a fact $f$ is true at time $t$, then there must exist an action having $f$ as its add-effect which is true at time $t-1$.

%\item Delete effects of simple actions (for all $a\in O^s$,~$0\le t < N$):
%$$x_{a,t}\to \bigwedge_{\forall f, f\in del(a)} \neg x_{f,t+1}$$
%An action is true at time $t$, then all its delete-effects can't be ture at time $t+1$.

\item Durative actions ($\forall o,t,~o\in O$,~$0\le t < t+\rho < N$):
$$ x_{o_{\vdash},t } \leftrightarrow x_{o_{\dashv},t+\rho-1}$$
$$ x_{o_{\vdash},t} \rightarrow \bigwedge_{t+1 \leq t' \leq t+\rho-1} ( x_{ f^o, t'} )$$
$$ x_{o_{\vdash},t} \rightarrow \bigwedge_{t+1 \leq t' \leq t+\rho-1} ( \bigwedge_{f \in \pi_{\leftrightarrow}} x_{f,t'} )$$
%$ x_{o_{\vdash},t} \rightarrow \bigwedge_{t<t'<t+\rho-1,f\in
%o_{\leftrightarrow}  } x_{ f^o, t'}$
%Qiang ??? not quite understand.
If a start action $o_{\vdash}$ is true at time $t$, then action $o_{\dashv}$ must be true at time $t+\rho-1$, and vice versa.
If a start action $o_{\vdash}$ is true at time $t$, then the fact $f^o$ and all the overall facts determined by $\pi_{\leftrightarrow}$ must be true in the executing duration $[t+1, t+\rho-1]$.
These constraints enforce that $o$ is executed in $[t, t+\rho)$. 
Note it is not necessary to encode this type of constraints for those actions whose duration $\rho$ is smaller than or equal to 1.

%\item Axioms (for each $a\in A$,$0\le t\le N$): \\
%    $\bigwedge_{f\in pre(a)}(x_{f,t})\rightarrow \bigwedge_{f'\in \textit{eff}(a)}(x_{f',t})$

\item Action mutexes ($0\le t < N$): for each pair of  mutex actions $(a_1,a_2)$:
    $$\neg x_{a_1,t} \bigvee \neg x_{a_2,t}$$
These clauses indicate that those mutex actions cannot be true at the same time.

\item Fact mutexes ($0\le t \le N$): for each pair of mutex facts $(f_1,f_2)$:
    $$\neg x_{f_1,t} \bigvee \neg x_{f_2,t}$$
These clauses indicate that those mutex facts cannot be true at the same time.
\end{enumerate}

Since the transformed problem is a classical planning problem with additional temporal constraints, the encoding introduced above shares many similarities to the well know STRIPS encoding~\cite{Kautz92} except for clauses in class (5).
For a given valid assignment $\psi$, the corresponding plan sequence $P=(p_0,p_1, \cdots, p_{N-1})$ and states $S_0, S_1, \cdots, S_N$, we have:
\begin{itemize}
\item Clauses in class (1) guarantee that $S_0=I$.
\item For each action $o_t\in p_t$, clauses in class (3) of actions $a=o_{\vdash}, o_{\dashv}$ and clauses (5) of overall facts make sure that $o_t$ is applicable at time $t$.
Clauses (4) make sure $S_{t+1},~S_{t+\rho(o)}$ satisfy $o_t$'s add-effects.
Similar to the SATPlan encoding for classical STRIPS planning~\cite{Kautz04}, our mutex clauses guarantee the consistence of delete effects.
All mutex relations between facts and actions are detected based on the algorithm in~\cite{Smith99}.
Clauses in classes (6) and (7) make sure that $S_{t+1},~S_{t+\rho(o)}$ satisfy $o$'s delete effects at time $t$.
Therefore, for each action $o_t\in p_t$,  $o_t$ is applicable at time $t$, and $S_{t+1},~S_{t+\rho(o)}$ satisfy $o_t$'s effects.
\item Clauses (2) make sure that for all $f\in G$, $f_N\in S_N$.
\end{itemize}
According to Definition~\ref{def:plan}, $P$ is a solution plan of the CSTE problem.
Therefore, any plan derived from a satisfying assignment of $\Phi$ is a solution plan for CSTE problem $\Pi$.


The encoding above produces a standard SAT problem.
The cost of each variable $x \in V$ in a MinCost SAT problem
$\Phi^c=(V,C,\mu)$ is defined as:
\[ \mu(x) = \left  \{
\begin{array}{ll}
   \mu(o),       & \mbox{if $x=x_{o_{{\vdash},t}}$ for some action $o\in O$ and a time step $t$ } \\
    0,          & \mbox{otherwise}\\
\end{array} \right. \]
In other words, for each action $o$ whose cost is $\mu(o)$, we make the
corresponding variable $x_{o_{\vdash},t}$ to have a cost $\mu(o)$. All
other variables have zero costs.


\nop{
Our approach is not only effective for handling temporally
expressive semantics, but also capable of accommodating some other
attributes of parallelism in temporal planning. According to the
analysis in~\cite{Rintanen07:AAAI}, whether a temporal planning
problem can be compiled into a classical planning problem in
polynomial time is determined by whether or not self-overlapping is
allowed.  Our approach supports self overlapping.
}
%YC: I don't understand this sentence and why this is useful here.
%For a given action $o$ and time $t$, we have variables
%$x_{o_{\vdash},t}$ and $x_{o_{\dashv},t}$ representing the starting
%and ending actions of $o$, respectively.

Suppose that in a plan, an action $o$ (with duration $\rho$) has two
instances, starting at times $t$ and $t'$ ($t<t'$), respectively. To
initiate actions, we have different variables $x_{o_{\vdash},t}$ and
$x_{o_{\vdash},t'}$ to indicate the different starting times of the
two instances. Those $f^o$ facts, along with all related conditions,
will be enforced to be true from $t+1$ to $t+\rho-1$ and $t'+1$ to $t'+\rho-1$, even if they have overlapping durations.
Thus, these invariant conditions of the two action instances do not exclude each
other's existence.

Note that the new encoding cannot handle the special case when the two
instances of an action start at the same time. This is because given
a simple action $o_{\vdash}$, for each time point $t$, we have only one
Boolean variable $x_{o_{\vdash},t}$to indicate if $o$ is executed at $t$.
%= o_{\vdash} or o_{\dashv}$,
